\begin{tabbing}
$\forall$\=${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $p$:($\forall$$e$:E. Dec($P$($e$))), $Q$, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$),\+
\\[0ex]${\it Ib}$:AbsInterface($B$), $f$:(E(${\it Ia}$)$\rightarrow$$B$), $g$:(E(${\it Ib}$)$\rightarrow$E).
\-\\[0ex]($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ ${\it Ib}$)) $\Rightarrow$ $P$($e$)) $\Rightarrow$ $g$ glues ${\it Ia}$:$Q$ $--$$f$$\rightarrow$ (${\it Ib}$$\mid$$p$):$R$ $\Rightarrow$ $g$ glues ${\it Ia}$:$Q$ $--$$f$$\rightarrow$ ${\it Ib}$:$R$
\end{tabbing}